es:ES, e, e':E, l:IdLnk.
(e'  es-receives(es;e;l))  isrcv(e') & sender(e') = e & lnk(e') = l 

latex

Definitions

es-receives(es;e;l), (x  l), lnk(e), sender(e), x:AB(x), isrcv(e), Type, Prop, A & B, P  Q, P  Q, f(a), Unit, left+right, first(e), A, IdLnkDeq, es-eq(es), Void, x:AB(x), False, rcv-from-on(dE;dL;info;e;l;r), {x:A| B(x) }, type List, S  T, receives(dE;dL;pred?;info;p;e;l), EOrderAxioms(E; pred?; info), ES, es_info(es), es-pred?(es), E, pred!(e;e'), SWellFounded(R(x;y)), es-oaxioms(es), 1of(t), destination(l), loc(e), Id, s = t, e < e', P  Q, P & Q, link(e), IdLnk, P  Q, sender(e), rcv?(e), b, x:A. B(x), x:A. B(x), t  T, loc(e), pred(e), first(e), kind(e), lnk(k), isrcv(k), kind(e)

Lemmas

isrcv wf, lnk wf, kind wf, rcv?-link, rcv?-kind, es-loc-pred, event system wf, es-oaxioms wf, EOrderAxioms wf, es-pred!-wellfounded, iff functionality wrt iff, member receives, receives wf, rcv-from-on wf, es-eq wf, idlnk-deq wf, not wf, first wf, unit wf, es-pred? wf, loc wf, rcv? wf, sender wf, link wf, Id wf, es info wf, assert wf, es-isrcv wf, es-sender wf, IdLnk wf, es-lnk wf, l member wf, es-E wf, es-receives wf